\begin{tabbing}
ecl{-}trans{-}tuple\=\{i:l\}\+
\\[0ex](${\it ds}$; ${\it da}$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$T$:Type\{i\}\+
\\[0ex]$\times$ (${\it ks}$:(Knd List)
\\[0ex]$\times$ :$T$
\\[0ex]$\times$ :($k$:\{$k$:Knd$\mid$ ($k$ $\in$ ${\it ks}$ $\in$ Knd)\} $\rightarrow$decl{-}state(${\it ds}$)$\rightarrow$ma{-}valtype(${\it da}$; $k$)$\rightarrow$$T$$\rightarrow$$T$)
\\[0ex]$\times$ :($\mathbb{N}\rightarrow$$T$$\rightarrow\mathbb{B}$)
\\[0ex]$\times$ (:($\mathbb{N}\rightarrow$($k$:\{$k$:Knd$\mid$ ($k$ $\in$ ${\it ks}$ $\in$ Knd)\} $\rightarrow$decl{-}state(${\it ds}$)$\rightarrow$ma{-}valtype(${\it da}$; $k$)$\rightarrow$$T$$\rightarrow\mathbb{B}$))
\\[0ex]$\times$ ($\mathbb{N}^{+}$ List)))
\-
\end{tabbing}